Skip to content

docs(status): first populated rows in the cross-prover register — squeakwell recovery ladder - #32

Merged
hyperpolymath merged 3 commits into
mainfrom
claude/gracious-darwin-vkgj6l
Nov 10, 2026
Merged

docs(status): first populated rows in the cross-prover register — squeakwell recovery ladder#32
hyperpolymath merged 3 commits into
mainfrom
claude/gracious-darwin-vkgj6l

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented Nov 9, 2026

Copy link
Copy Markdown
Owner

Summary

Populates the register in docs/status/CROSS-PROVER-RECONCILIATION.adoc with its first real rows: the hyperpolymath/squeakwell recovery ladder, whose rungs now have prover-checked artefacts in their estate homes. Statuses are correspondence states only, per the policy's own vocabulary; no grade is written into a status field, and nothing is marked RECONCILED.

Changes

  • Four register rows:
    • R3/R9 merge laws — AGDA-VERIFIED (echo-types EchoPartialSection.agda, Agda 2.7.0.1, pinned stdlib/absolute-zero) / COQ-CHECKED (verisimdb formal/Recovery.v, Coq 8.18.0) / BRIDGE-PENDING: the relation is a refinement (Agda pointwise, Rocq function equality under functional_extensionality_dep).
    • R8 narrowing — AGDA-VERIFIED (EchoFibreIntersection.agda); single-prover.
    • R10 progress/termination — COQ-CHECKED (Recovery.v) / AGDA-PENDING.
    • R5–R7 — LEAN-CHECKED (tropical-types Resource/HubCeiling.lean, Lean 4.35.0; axioms propext/Quot.sound only) / AGDA-PENDING / BRIDGE-PENDING.
  • A dated preamble: these were checked in one local session; the owning repositories' CI must confirm on merge (verisimdb#350, tropical-types#67, the echo-types PR); the per-rung receipts live in squeakwell PROOF-STATUS.adoc.
  • :revdate: moved to 2026-11-09.
  • The census-generated catalogue is deliberately not hand-edited; it picks up the new proof files when the census is rerun after those PRs merge.

RSR Quality Checklist

Required

  • Tests pass (docs-only change; no test surface touched)
  • Code is formatted (AsciiDoc; table cells checked for stray |)
  • Linter is clean
  • No banned language patterns
  • No unsafe blocks without // SAFETY: comments
  • No banned functions
  • SPDX license headers present on all new/modified source files
  • No secrets, credentials, or .env files included

As Applicable

  • Repo deed (status) / (maturity) updated (no project-state change)
  • Repo deed (ecosystem) updated (no integration change)
  • Repo deed (meta) / docs/decisions/ updated (no architectural decision)
  • docs/status/ROADMAP.adoc updated (no milestone change; the register is the record)
  • Documentation updated for user-facing changes
  • TOPOLOGY.md updated (n/a)
  • CHANGELOG or release notes updated (status doc carries its own revdate)
  • New dependencies reviewed (none)
  • ABI/FFI changes validated (n/a)

Testing

Rendered the edited table region by eye for cell delimiters; the only | inside a cell was replaced with prose. Receipts for the underlying proofs (toolchains, commands, results) are in squeakwell PROOF-STATUS.adoc and in the three linked PRs.

Screenshots

n/a

Generated by Claude Code

@hyperpolymath @claude
docs(status): first populated rows in the cross-prover register — squ…
3e2db9f 
…eakwell recovery ladder

Adds four rows to the register in CROSS-PROVER-RECONCILIATION.adoc for the
hyperpolymath/squeakwell recovery ladder, with correspondence states only
(no grades written into status fields):

- R3/R9 merge laws: AGDA-VERIFIED (echo-types EchoPartialSection.agda,
  Agda 2.7.0.1, pinned libraries) / COQ-CHECKED (verisimdb
  formal/Recovery.v, Coq 8.18.0) / BRIDGE-PENDING — the relation is a
  refinement (pointwise vs. function equality under funext), not
  same-statement.
- R8 narrowing: AGDA-VERIFIED (EchoFibreIntersection.agda); single-prover.
- R10 progress/termination: COQ-CHECKED (Recovery.v) / AGDA-PENDING.
- R5–R7: LEAN-CHECKED (tropical-types Resource/HubCeiling.lean, Lean
  4.35.0) / AGDA-PENDING / BRIDGE-PENDING.

A dated preamble says these were checked in one local session and that
the owning repositories' CI must confirm them on merge; none is
RECONCILED. The census-generated catalogue is left for the census rerun.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8
@coderabbitai

coderabbitai Bot commented Nov 9, 2026 •
edited
Loading

Copy link
Copy Markdown

Explain Change →

Caution

Review failed

The pull request is closed.

  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

@claude
docs(architecture): regenerate REPOSITORY-MAP for the applied-systems…
df95924 
… tree

`just repo-map` output; the committed map predates the applied-systems/
directories added on main (2026-11-07), so the estate-rules
repo_map_determinism_test fails on main and on every branch from it. Pure
regeneration, additive only; no-op once main carries the same.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDizuhJtQDcxHxM2wj8
@hyperpolymath Claude

hyperpolymath commented Nov 9, 2026

Copy link
Copy Markdown
Owner Author

Two red checks on this PR, both red on main (a3dbe73, run 42592013824 and 42592014015) before this branch existed; this PR changes one AsciiDoc file under docs/status/.

  • estate-rules — repo_map_determinism_test.sh: the committed REPOSITORY-MAP.adoc predates the applied-systems/ tree added on main on 2026-11-07. Fix ported here in df95924: just repo-map regeneration (9 additive lines); the test passes locally and the commit no-ops once main carries the same regeneration.
  • Dogfood Gate / Canon lockstep — mathesis_chora.deed declares criteria-sha256/gates-sha256/version pins that no longer match canon.lock at standards HEAD. That is a canon version bump in the deed, an owner decision under the estate's no-automated-canon-edit rule, so not fixed from this PR. No fix PR exists yet on main.

Generated by Claude Code

@hyperpolymath
hyperpolymath marked this pull request as ready for review November 9, 2026 15:43
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Nov 9, 2026

Copy link
Copy Markdown
Codex Review Summary: ❌ Failed

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ❌ Failed 2026-11-09T15:43:31.143136Z
We couldn’t complete this review. Comment @codex review to try again.		 df95924 Draft marked ready
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Nov 9, 2026

Copy link
Copy Markdown

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

@hyperpolymath hyperpolymath assigned Copilot and unassigned Copilot Nov 9, 2026
@hyperpolymath
hyperpolymath merged commit 820d354 into main Nov 10, 2026
38 of 39 checks passed
@sonarqubecloud

sonarqubecloud Bot commented Nov 10, 2026

Copy link
Copy Markdown

Quality Gate Passed Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

Copilot code review Copilot

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@hyperpolymath @claude